; benchmark generated from python API
(set-info :status unknown)
(declare-fun title_bg_feasible () Bool)
(declare-fun title_bg_kid_8_feasible () Bool)
(declare-fun title_bg_kid_7_feasible () Bool)
(declare-fun title_bg_kid_6_feasible () Bool)
(declare-fun title_bg_kid_5_feasible () Bool)
(declare-fun title_bg_kid_4_feasible () Bool)
(declare-fun title_bg_kid_3_feasible () Bool)
(declare-fun title_bg_kid_2_feasible () Bool)
(declare-fun title_bg_kid_1_feasible () Bool)
(declare-fun title_bg_kid_0_feasible () Bool)
(declare-fun title_bg_kid_8_y () Real)
(declare-fun title_bg_hight () Real)
(declare-fun title_bg_kid_8_hight () Real)
(declare-fun title_bg_kid_7_hight () Real)
(declare-fun title_bg_kid_7_y () Real)
(declare-fun title_bg_kid_6_hight () Real)
(declare-fun title_bg_kid_6_y () Real)
(declare-fun title_bg_kid_5_hight () Real)
(declare-fun title_bg_kid_5_y () Real)
(declare-fun title_bg_kid_4_hight () Real)
(declare-fun title_bg_kid_4_y () Real)
(declare-fun title_bg_kid_3_hight () Real)
(declare-fun title_bg_kid_3_y () Real)
(declare-fun title_bg_kid_2_y () Real)
(declare-fun title_bg_kid_2_hight () Real)
(declare-fun title_bg_kid_1_y () Real)
(declare-fun title_bg_kid_1_hight () Real)
(declare-fun title_bg_kid_0_hight () Real)
(declare-fun title_bg_kid_0_y () Real)
(declare-fun title_bg_kid_0_width () Real)
(declare-fun title_bg_kid_8_width () Real)
(declare-fun title_bg_kid_7_width () Real)
(declare-fun title_bg_kid_6_width () Real)
(declare-fun title_bg_kid_5_width () Real)
(declare-fun title_bg_kid_4_width () Real)
(declare-fun title_bg_kid_3_width () Real)
(declare-fun title_bg_kid_2_width () Real)
(declare-fun title_bg_kid_1_width () Real)
(declare-fun title_bg_kid_0_x () Real)
(declare-fun title_bg_kid_7_x () Real)
(declare-fun title_bg_kid_1_x () Real)
(declare-fun title_bg_kid_8_x () Real)
(declare-fun title_bg_kid_6_x () Real)
(declare-fun title_bg_kid_5_x () Real)
(declare-fun title_bg_kid_4_x () Real)
(declare-fun title_bg_kid_3_x () Real)
(declare-fun title_bg_kid_2_x () Real)
(declare-fun title_bg_width () Real)
(assert
 (let (($x1977 (= (+ (- title_bg_kid_8_hight title_bg_hight) title_bg_kid_8_y) (- 10.0))))
 (let (($x1974 (= title_bg_kid_8_y 10.0)))
 (let (($x1973 (= (- (+ title_bg_kid_7_y title_bg_kid_7_hight) title_bg_hight) (- 10.0))))
 (let (($x1970 (= title_bg_kid_7_y 10.0)))
 (let (($x1969 (= (- (+ title_bg_kid_6_y title_bg_kid_6_hight) title_bg_hight) (- 10.0))))
 (let (($x1966 (= title_bg_kid_6_y 10.0)))
 (let (($x1965 (= (- (+ title_bg_kid_5_y title_bg_kid_5_hight) title_bg_hight) (- 10.0))))
 (let (($x1962 (= title_bg_kid_5_y 10.0)))
 (let (($x1961 (= (- (+ title_bg_kid_4_y title_bg_kid_4_hight) title_bg_hight) (- 10.0))))
 (let (($x1958 (= title_bg_kid_4_y 10.0)))
 (let (($x1957 (= (+ (- title_bg_kid_3_y title_bg_hight) title_bg_kid_3_hight) (- 10.0))))
 (let (($x1954 (= title_bg_kid_3_y 10.0)))
 (let (($x1953 (= (+ (- title_bg_kid_2_hight title_bg_hight) title_bg_kid_2_y) (- 10.0))))
 (let (($x1950 (= title_bg_kid_2_y 10.0)))
 (let (($x1949 (= (+ (- title_bg_kid_1_hight title_bg_hight) title_bg_kid_1_y) (- 10.0))))
 (let (($x1946 (= title_bg_kid_1_y 10.0)))
 (let (($x1945 (= (- (+ title_bg_kid_0_y title_bg_kid_0_hight) title_bg_hight) (- 10.0))))
 (let (($x1942 (= title_bg_kid_0_y 10.0)))
 (let (($x1941 (= title_bg_kid_0_width 100.0)))
 (let (($x1940 (= (+ (- title_bg_kid_8_width) title_bg_kid_0_width) 0.0)))
 (let (($x1937 (= (+ (- title_bg_kid_7_width) title_bg_kid_0_width) 0.0)))
 (let (($x1934 (= (- title_bg_kid_0_width title_bg_kid_6_width) 0.0)))
 (let (($x1932 (= (+ (- title_bg_kid_5_width) title_bg_kid_0_width) 0.0)))
 (let (($x1930 (= (+ (- title_bg_kid_4_width) title_bg_kid_0_width) 0.0)))
 (let (($x1928 (= (+ (- title_bg_kid_3_width) title_bg_kid_0_width) 0.0)))
 (let (($x1925 (= (+ (- title_bg_kid_2_width) title_bg_kid_0_width) 0.0)))
 (let (($x1922 (= (+ (- title_bg_kid_1_width) title_bg_kid_0_width) 0.0)))
 (let ((?x1916 (+ (- (- title_bg_kid_8_x title_bg_kid_1_x) title_bg_kid_7_x) title_bg_kid_0_x)))
 (let (($x1919 (= (+ (- ?x1916 title_bg_kid_7_width) title_bg_kid_0_width) 0.0)))
 (let ((?x1910 (- (+ (+ (- title_bg_kid_1_x) title_bg_kid_7_x) title_bg_kid_0_x) title_bg_kid_6_x)))
 (let (($x1913 (= (- (+ ?x1910 title_bg_kid_0_width) title_bg_kid_6_width) 0.0)))
 (let ((?x1904 (- (+ (- (- title_bg_kid_5_width) title_bg_kid_1_x) title_bg_kid_0_x) title_bg_kid_5_x)))
 (let (($x1907 (= (+ (+ ?x1904 title_bg_kid_6_x) title_bg_kid_0_width) 0.0)))
 (let ((?x1898 (+ (+ (- (- title_bg_kid_4_width) title_bg_kid_1_x) title_bg_kid_0_x) title_bg_kid_5_x)))
 (let (($x1901 (= (- (+ ?x1898 title_bg_kid_0_width) title_bg_kid_4_x) 0.0)))
 (let ((?x1892 (+ (- (- (- title_bg_kid_3_x) title_bg_kid_1_x) title_bg_kid_3_width) title_bg_kid_0_x)))
 (let (($x1895 (= (+ (+ ?x1892 title_bg_kid_0_width) title_bg_kid_4_x) 0.0)))
 (let ((?x1886 (+ (- (- title_bg_kid_3_x title_bg_kid_1_x) title_bg_kid_2_x) title_bg_kid_0_x)))
 (let (($x1889 (= (+ (- ?x1886 title_bg_kid_2_width) title_bg_kid_0_width) 0.0)))
 (let ((?x1880 (+ (+ (* (- 2.0) title_bg_kid_1_x) title_bg_kid_2_x) title_bg_kid_0_x)))
 (let (($x1883 (= (+ (- ?x1880 title_bg_kid_1_width) title_bg_kid_0_width) 0.0)))
 (let (($x1877 (= (+ (+ (- title_bg_width) title_bg_kid_8_x) title_bg_kid_8_width) (- 10.0))))
 (let (($x1873 (= title_bg_kid_0_x 10.0)))
 (let (($x1872 (>= (- (- title_bg_kid_8_x title_bg_kid_7_x) title_bg_kid_7_width) 0.0)))
 (let (($x1869 (>= (- (- title_bg_kid_7_x title_bg_kid_6_x) title_bg_kid_6_width) 0.0)))
 (let (($x1866 (>= (+ (- (- title_bg_kid_5_width) title_bg_kid_5_x) title_bg_kid_6_x) 0.0)))
 (let (($x1863 (>= (- (+ (- title_bg_kid_4_width) title_bg_kid_5_x) title_bg_kid_4_x) 0.0)))
 (let (($x1860 (>= (+ (- (- title_bg_kid_3_x) title_bg_kid_3_width) title_bg_kid_4_x) 0.0)))
 (let (($x1857 (>= (- (- title_bg_kid_3_x title_bg_kid_2_x) title_bg_kid_2_width) 0.0)))
 (let (($x1854 (>= (- (+ (- title_bg_kid_1_x) title_bg_kid_2_x) title_bg_kid_1_width) 0.0)))
 (let (($x1850 (>= (- (- title_bg_kid_1_x title_bg_kid_0_x) title_bg_kid_0_width) 0.0)))
 (let (($x1847 (>= (- (+ (- title_bg_kid_8_hight) title_bg_hight) title_bg_kid_8_y) 10.0)))
 (let (($x1843 (>= title_bg_kid_8_y 10.0)))
 (let (($x1842 (>= (- (- title_bg_width title_bg_kid_8_x) title_bg_kid_8_width) 10.0)))
 (let (($x1839 (>= title_bg_kid_8_x 10.0)))
 (let (($x1838 (>= (+ (- (- title_bg_kid_7_y) title_bg_kid_7_hight) title_bg_hight) 10.0)))
 (let (($x1834 (>= title_bg_kid_7_y 10.0)))
 (let (($x1833 (>= (- (- title_bg_width title_bg_kid_7_x) title_bg_kid_7_width) 10.0)))
 (let (($x1830 (>= title_bg_kid_7_x 10.0)))
 (let (($x1829 (>= (+ (- (- title_bg_kid_6_y) title_bg_kid_6_hight) title_bg_hight) 10.0)))
 (let (($x1825 (>= title_bg_kid_6_y 10.0)))
 (let (($x1824 (>= (- (- title_bg_width title_bg_kid_6_x) title_bg_kid_6_width) 10.0)))
 (let (($x1821 (>= title_bg_kid_6_x 10.0)))
 (let (($x1820 (>= (+ (- (- title_bg_kid_5_y) title_bg_kid_5_hight) title_bg_hight) 10.0)))
 (let (($x1816 (>= title_bg_kid_5_y 10.0)))
 (let (($x1815 (>= (- (+ (- title_bg_kid_5_width) title_bg_width) title_bg_kid_5_x) 10.0)))
 (let (($x1811 (>= title_bg_kid_5_x 10.0)))
 (let (($x1810 (>= (+ (- (- title_bg_kid_4_y) title_bg_kid_4_hight) title_bg_hight) 10.0)))
 (let (($x1806 (>= title_bg_kid_4_y 10.0)))
 (let (($x1805 (>= (- (+ (- title_bg_kid_4_width) title_bg_width) title_bg_kid_4_x) 10.0)))
 (let (($x1801 (>= title_bg_kid_4_x 10.0)))
 (let (($x1800 (>= (- (+ (- title_bg_kid_3_y) title_bg_hight) title_bg_kid_3_hight) 10.0)))
 (let (($x1796 (>= title_bg_kid_3_y 10.0)))
 (let (($x1795 (>= (- (+ (- title_bg_kid_3_x) title_bg_width) title_bg_kid_3_width) 10.0)))
 (let (($x1791 (>= title_bg_kid_3_x 10.0)))
 (let (($x1790 (>= (- (+ (- title_bg_kid_2_hight) title_bg_hight) title_bg_kid_2_y) 10.0)))
 (let (($x1786 (>= title_bg_kid_2_y 10.0)))
 (let (($x1785 (>= (- (- title_bg_width title_bg_kid_2_x) title_bg_kid_2_width) 10.0)))
 (let (($x1782 (>= title_bg_kid_2_x 10.0)))
 (let (($x1781 (>= (- (+ (- title_bg_kid_1_hight) title_bg_hight) title_bg_kid_1_y) 10.0)))
 (let (($x1777 (>= title_bg_kid_1_y 10.0)))
 (let (($x1776 (>= (- (- title_bg_width title_bg_kid_1_x) title_bg_kid_1_width) 10.0)))
 (let (($x1773 (>= title_bg_kid_1_x 10.0)))
 (let (($x1772 (>= (+ (- (- title_bg_kid_0_y) title_bg_kid_0_hight) title_bg_hight) 10.0)))
 (let (($x1768 (>= title_bg_kid_0_y 10.0)))
 (let (($x1767 (>= (- (- title_bg_width title_bg_kid_0_x) title_bg_kid_0_width) 10.0)))
 (let (($x1764 (>= title_bg_kid_0_x 10.0)))
 (let (($x1763 (>= title_bg_kid_8_hight 0.0)))
 (let (($x1762 (>= title_bg_kid_8_width 0.0)))
 (let (($x1761 (>= title_bg_kid_8_y 0.0)))
 (let (($x1760 (>= title_bg_kid_8_x 0.0)))
 (let (($x1759 (>= title_bg_kid_7_hight 0.0)))
 (let (($x1758 (>= title_bg_kid_7_width 0.0)))
 (let (($x1757 (>= title_bg_kid_7_y 0.0)))
 (let (($x1756 (>= title_bg_kid_7_x 0.0)))
 (let (($x1755 (>= title_bg_kid_6_hight 0.0)))
 (let (($x1754 (>= title_bg_kid_6_width 0.0)))
 (let (($x1753 (>= title_bg_kid_6_y 0.0)))
 (let (($x1752 (>= title_bg_kid_6_x 0.0)))
 (let (($x1751 (>= title_bg_kid_5_hight 0.0)))
 (let (($x1750 (>= title_bg_kid_5_width 0.0)))
 (let (($x1749 (>= title_bg_kid_5_y 0.0)))
 (let (($x1748 (>= title_bg_kid_5_x 0.0)))
 (let (($x1747 (>= title_bg_kid_4_hight 0.0)))
 (let (($x1746 (>= title_bg_kid_4_width 0.0)))
 (let (($x1745 (>= title_bg_kid_4_y 0.0)))
 (let (($x1744 (>= title_bg_kid_4_x 0.0)))
 (let (($x1743 (>= title_bg_kid_3_hight 0.0)))
 (let (($x1742 (>= title_bg_kid_3_width 0.0)))
 (let (($x1741 (>= title_bg_kid_3_y 0.0)))
 (let (($x1740 (>= title_bg_kid_3_x 0.0)))
 (let (($x1739 (>= title_bg_kid_2_hight 0.0)))
 (let (($x1738 (>= title_bg_kid_2_width 0.0)))
 (let (($x1737 (>= title_bg_kid_2_y 0.0)))
 (let (($x1736 (>= title_bg_kid_2_x 0.0)))
 (let (($x1735 (>= title_bg_kid_1_hight 0.0)))
 (let (($x1734 (>= title_bg_kid_1_width 0.0)))
 (let (($x1733 (>= title_bg_kid_1_y 0.0)))
 (let (($x1732 (>= title_bg_kid_1_x 0.0)))
 (let (($x1731 (>= title_bg_kid_0_hight 0.0)))
 (let (($x1730 (>= title_bg_kid_0_width 0.0)))
 (let (($x1729 (>= title_bg_kid_0_y 0.0)))
 (let (($x1728 (>= title_bg_kid_0_x 0.0)))
 (and $x1728 $x1729 $x1730 $x1731 $x1732 $x1733 $x1734 $x1735 $x1736 $x1737 $x1738 $x1739 $x1740 $x1741 $x1742 $x1743 $x1744 $x1745 $x1746 $x1747 $x1748 $x1749 $x1750 $x1751 $x1752 $x1753 $x1754 $x1755 $x1756 $x1757 $x1758 $x1759 $x1760 $x1761 $x1762 $x1763 $x1764 $x1767 $x1768 $x1772 $x1773 $x1776 $x1777 $x1781 $x1782 $x1785 $x1786 $x1790 $x1791 $x1795 $x1796 $x1800 $x1801 $x1805 $x1806 $x1810 $x1811 $x1815 $x1816 $x1820 $x1821 $x1824 $x1825 $x1829 $x1830 $x1833 $x1834 $x1838 $x1839 $x1842 $x1843 $x1847 $x1850 $x1854 $x1857 $x1860 $x1863 $x1866 $x1869 $x1872 $x1873 $x1877 $x1883 $x1889 $x1895 $x1901 $x1907 $x1913 $x1919 $x1922 $x1925 $x1928 $x1930 $x1932 $x1934 $x1937 $x1940 $x1941 $x1942 $x1945 $x1946 $x1949 $x1950 $x1953 $x1954 $x1957 $x1958 $x1961 $x1962 $x1965 $x1966 $x1969 $x1970 $x1973 $x1974 $x1977 title_bg_kid_0_feasible title_bg_kid_1_feasible title_bg_kid_2_feasible title_bg_kid_3_feasible title_bg_kid_4_feasible title_bg_kid_5_feasible title_bg_kid_6_feasible title_bg_kid_7_feasible title_bg_kid_8_feasible title_bg_feasible)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

